M:MsgA. Feasible(M)  (k:Knd. AtomFree(Type;M.da(k))) 

latex

Definitions	t  T, P  Q, x:A. B(x), xdom(f). v=f(x)   P(x;v), Top, Void, x:A. B(x), Type, AtomFree(T;x), P & Q, b, A, b, , s = t, Prop, Knd, x.A(x), x. t(x), a:A fp B(a), x:AB(x), KindDeq, x  dom(f), x:AB(x), P  Q, Unit, left+right, f(x)?z, Valtype(da;k), M.sframe(k sends <l,tg>), M.frame(k affects x), M.da(a), MsgA, Feasible(M)
Lemmas	ma-feasible wf, msga wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, bool wf, bnot wf, not wf, assert wf, top wf